00100	The following improvements in the proof checker are required.
00200	
00300		1. Conditional expressions should be
00400	terms and not just propositional expressions.
00500	
00600	2. We need an axiom schema of comprehension.  I can explain this
00700	precisely.
00800	
00900	3. λ-introduction.  I have not yet tried to use λ-elimination.
01000	
01100	4. A rule allowing assertion of the result of a computation.
01200	
01300	5. A rule allowing the assertion of
01400	
01500		value((CAR X)) = car(x)
01600	
01700	and such like things.  I don't see the full desired scope of the
01800	rule yet, but it should also handle truth.
01900	
02000	6*. A rule allowing relativization of proofs to a given domain.
02100	The proof that x'+y = (x+y)' could be greatly reduced in size
02200	if this were done.
02300	
02400	7. Fix the bug that allows illegitimate replacements.
02500